decl{-}type\{i:l\}(${\it ds}$; $x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}cap(${\it ds}$; id{-}deq; $x$; void)